$\forall$$T$:Type, ${\it eq}$:($T$$\rightarrow$$T$$\rightarrow\mathbb{B}$). eq\_seq(${\it eq}$) $\in$ $k$:$\mathbb{N}\times$($\mathbb{N}$$_{\mbox{\scriptsize $<$$k$}}$$\rightarrow$$T$)$\rightarrow$$k$:$\mathbb{N}\times$($\mathbb{N}$$_{\mbox{\scriptsize $<$$k$}}$$\rightarrow$$T$)$\rightarrow\mathbb{B}$